Nuprl Lemma : imax_lb
13,42
postcript
pdf
a
,
b
,
c
:
. (imax(
a
;
b
)
c
)
{(
a
c
) & (
b
c
)}
latex
Up
int
2
,
int
2
Definitions
True
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
a, b, c:
. (imax(a;b) 
c) 
{(a c) & (b c)} a, b, c:. (imax(a;b) c) {(a c) & (b c)} Q Q Q
Tx:A. B(x)